As embedded systems continue to face increasingly higher performance requirements, deeply pipelined processor architectures are being employed to meet desired system performance. Functional validation of such programmable processors is one of the most complex and expensive tasks in the current Systems-on-Chip (SOC) design methodology. Simulation is the most widely used form of microprocessor verification: millions of cycles are spent during simulation using a combination of random and directed test cases in traditional validation flow. Several coverage measures are commonly used, such as code coverage, toggle coverage and fault coverage, to attempt to ensure that all aspects of a microprocessor design have been validated by the simulation. Unfortunately, these measures do not have any direct relationship to the functionality of the device. For example, none of these measures determine if all possible interactions of hazards, stalls and exceptions are tested in a processor pipeline. Additionally, certain heuristics and design abstractions are used to generate directed random test cases. However, due to the bottom-up nature and localized view of these heuristics the generated test cases may not yield a good coverage. The problem is further aggravated due to the lack of a comprehensive functional coverage metric.
Specification driven test generation has been introduced as a top-down validation technique for pipelined processors. The processor is specified using an Architecture Description Language (ADL). A SMV (Symbolic Model Verifier) description of the processor is generated from the ADL specification of the architecture. The SMV system is a tool for checking finite state systems against logic specifications for those systems. Further details about SMV are available in K. L. McMillan, The SMV System for SMV version 2.5.4. Specific properties are applied to the processor model using the SMV model checker. For example, to generate a test case to stall the decode unit, the property states that the decode unit is not stalled. The model checker produces a counter-example that stalls the decode unit. The generated counterexample is converted into a test program consisting of processor instructions. Since, the complete processor is modeled using SMV, this approach is limited by the capacity restrictions of the tool. As a result, it is not possible to model a detailed description of the processor and generate test programs which cover all of the functional aspects of the processor. Furthermore, the test generation time is long. Thus there is a need for a coverage metric based on the functionality of the processor design, and for which test program generation is automated.